#!/usr/bin/python

import re
import os
import sys
debug = True

lines = sys.stdin.readlines()
lemma = sys.argv[1]

# INPUT:
# - lines contain a list of "%i:goal" where "%i" is the index of the goal
# - lemma contain the name of the lemma under scrutiny
# OUTPUT:
# - (on stdout) a list of ordered index separated by EOL


rank = []             # list of list of goals, main list is ordered by priority
maxPrio = 110
for i in range(0,maxPrio):
  rank.append([])

# OBSERVATIONAL EQUIVALENCE LEMMA
if lemma == "Observational_equivalence":
  for line in lines:
    num = line.split(':')[0]

# for the simple passive game:
    if re.match('.*!Pk\(.*', line): rank[104].append(num)
    elif re.match('.* UE\( <.*', line): rank[103].append(num)
    elif re.match('.*~~>.*', line): rank[60].append(num)
    elif re.match('.*splitEqs\(.*', line): rank[50].append(num)
    elif re.match('.*!KD\(.*', line) and not(re.match('.*!KD\( x.*', line)) : rank[30].append(num)
    elif re.match('.*!KU\(.*', line) and not(re.match('.*!KU\( x.*', line)) : rank[20].append(num)

else:
  exit(0)

# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
  for goal in listGoals:
    sys.stderr.write(goal)
    print goal

